; COMMAND-LINE: --finite-model-find
(set-logic ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun tptp.environment ($$unsorted) Bool)
(declare-fun tptp.first_movers () $$unsorted)
(declare-fun tptp.efficient_producers () $$unsorted)
(declare-fun tptp.subpopulations ($$unsorted $$unsorted $$unsorted $$unsorted) Bool)
(declare-fun tptp.disbanding_rate ($$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.greater ($$unsorted $$unsorted) Bool)
(assert (not (forall ((E $$unsorted) (T $$unsorted)) (=> (and (tptp.environment E) (tptp.subpopulations tptp.first_movers tptp.efficient_producers E T)) (tptp.greater (tptp.disbanding_rate tptp.first_movers T) (tptp.disbanding_rate tptp.efficient_producers T))))))
(declare-fun tptp.founding_rate ($$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.greater_or_equal ($$unsorted $$unsorted) Bool)
(declare-fun tptp.growth_rate ($$unsorted $$unsorted) $$unsorted)
(assert (forall ((T $$unsorted)) (=> (and (tptp.greater (tptp.disbanding_rate tptp.first_movers T) (tptp.disbanding_rate tptp.efficient_producers T)) (tptp.greater_or_equal (tptp.founding_rate tptp.efficient_producers T) (tptp.founding_rate tptp.first_movers T))) (tptp.greater (tptp.growth_rate tptp.efficient_producers T) (tptp.growth_rate tptp.first_movers T)))))
(assert (forall ((X $$unsorted) (Y $$unsorted)) (=> (tptp.greater_or_equal X Y) (or (tptp.greater X Y) (= X Y)))))
(declare-fun tptp.stable ($$unsorted) Bool)
(declare-fun tptp.in_environment ($$unsorted $$unsorted) Bool)
(assert (forall ((E $$unsorted)) (=> (and (tptp.environment E) (tptp.stable E)) (exists ((To $$unsorted)) (and (tptp.in_environment E To) (forall ((T $$unsorted)) (=> (and (tptp.subpopulations tptp.first_movers tptp.efficient_producers E T) (tptp.greater_or_equal T To)) (tptp.greater_or_equal (tptp.founding_rate tptp.efficient_producers T) (tptp.founding_rate tptp.first_movers T)))))))))
(assert (not (forall ((E $$unsorted)) (=> (and (tptp.environment E) (tptp.stable E)) (exists ((To $$unsorted)) (and (tptp.in_environment E To) (forall ((T $$unsorted)) (=> (and (tptp.subpopulations tptp.first_movers tptp.efficient_producers E T) (tptp.greater_or_equal T To)) (tptp.greater (tptp.growth_rate tptp.efficient_producers T) (tptp.growth_rate tptp.first_movers T))))))))))
(set-info :filename MGT019+2)
(check-sat-assuming ( true ))
